A:Type, B:(AType), eq1, eq2:EqDecider(A), f:a:A fp B(a), x:A. x  dom(f) = x  dom(f)   

latex

Definitions	deq-member(eq;x;L), x. t(x), x(s), EqDecider(T), x  dom(f), a:A fp B(a), true, Unit, b, , false, P  Q, P & Q, Prop, b, t  T, (x  l), x:A. B(x), A, P  Q, False
Lemmas	l member wf, assert wf, assert-deq-member, not functionality wrt iff, bfalse wf, deq-member wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, btrue wf, bool wf, deq wf, fpf wf